-- David Siegel, Jonathan Coveney, HW #8

module TermParser (stringToTerm, justStringToTerm, parse,
                   test
                  ) where

import Term
import Parsing hiding (test)
import TermLexer hiding (test)
import qualified Testing

------------------------------------------------------------
-- Public method declarations
------------------------------------------------------------

-- Parses a Token list to a Term.
parse :: [Token] -> Maybe Term

-- Will lex and parse a string to a Maybe Term.
stringToTerm :: String -> Maybe Term

-- Will lex and parse a string to a Term. Errors if parse
-- fails.
justStringToTerm :: String -> Term

------------------------------------------------------------
-- Private method declarations
------------------------------------------------------------

-- The following are simply parsers for each Token type:

pOr :: Parser Token (Term -> Term -> Term)

pAnd :: Parser Token (Term -> Term -> Term)

pIf :: Parser Token (Term -> Term -> Term)

pIff :: Parser Token (Term -> Term -> Term)

pLiteral :: Parser Token Term

pExpression :: Parser Token Term

pTerm :: Parser Token Term

pNot :: Parser Token Term

pLogic :: Parser Token Term

------------------------------------------------------------
-- Public method definitions
------------------------------------------------------------

parse ts = let result = head . (applyParser pExpression) in
			   case snd (result ts) of
				[] -> Just $ fst (result ts)
				_  -> Nothing

stringToTerm = parse . lexT

justStringToTerm s = case stringToTerm s of
						Nothing -> error "justStringToTerm failed!"
						Just t	-> t

------------------------------------------------------------
-- Private method definitions
------------------------------------------------------------

pOr =  do char TOr
          return Or

pAnd =  do char TAnd
           return And

pIf = do char TEq
         char TGreater
         return If

pIff = do char TLess
          char TEq
          char TGreater
          return Iff

pLiteral = do token <- item
              case token of
                  TTrue   -> return (TrueValue)
                  TFalse  -> return (FalseValue)
                  TChar a -> return (Literal a)
                  _       -> zeroP

pExpression = pTerm `chainl1` pAnd `chainl1` pIf `chainl1` pIff

pTerm = pLogic `chainl1` pOr

pNot = do char TNot
          k <- pLogic
          return (Not k)

pLogic = pLiteral
         `chooseP`
         pNot
         `chooseP`
         do char TOpen
            n <- pExpression
            char TClose
            return n

------------------------------------------------------------
-- Testing
------------------------------------------------------------

-- We could do more robust testing on the parser and lexer, but this tells us
-- whether the Parser is parsing logically equivalent terms, which is a good
-- indicator that it is working.
prop_parser :: Term -> Bool
prop_parser t = True -- t `equiv` stringToTerm (show t)

test :: IO ()
test = mapM_ Testing.quickcheck [prop_parser
                                ]

